\relax 
\@writefile{toc}{\contentsline {title}{Modeling and Verification a PLC Design Pattern in Coq}{1}}
\@writefile{toc}{\authcount {1}}
\@writefile{toc}{\contentsline {author}{Hai Wan}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {2}Discussion of the old translation}{1}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces A sample of translating a LTS to PLC codes.}}{2}}
\newlabel{fig:example}{{1}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Description of the new translation}{2}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces An example of new transformation}}{3}}
\newlabel{fig:example}{{2}{3}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Modeling of the design pattern}{3}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces A SR flip-flop in PLC. Node 0 is S, node 2 is R and node 1 is the output of SR flip-flop.}}{5}}
\newlabel{fig:example}{{3}{5}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Verification of the design pattern}{6}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Conclusion}{7}}
